Termination w.r.t. Q proof of TRS/secret06nrOfNodes.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

COUNT(n, x) → ISEMPTY(left(n))
NROFNODES(n) → COUNT(n, 0)
COUNT(n, x) → LEFT(n)
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(n, x) → INC(x)
COUNT(n, x) → LEFT(left(n))
COUNT(n, x) → ISEMPTY(n)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
COUNT(n, x) → RIGHT(n)
COUNT(n, x) → RIGHT(left(n))
INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

COUNT(n, x) → ISEMPTY(left(n))
NROFNODES(n) → COUNT(n, 0)
COUNT(n, x) → LEFT(n)
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(n, x) → INC(x)
COUNT(n, x) → LEFT(left(n))
COUNT(n, x) → ISEMPTY(n)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
COUNT(n, x) → RIGHT(n)
COUNT(n, x) → RIGHT(left(n))
INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

NROFNODES(n) → COUNT(n, 0)
COUNT(n, x) → LEFT(n)
COUNT(n, x) → ISEMPTY(n)
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
COUNT(n, x) → RIGHT(left(n))
COUNT(n, x) → ISEMPTY(left(n))
COUNT(n, x) → LEFT(left(n))
COUNT(n, x) → INC(x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → RIGHT(n)
INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 8 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

INC(s(x)) → INC(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
INC(x1) = INC(x1)
s(x1) = s(x1)

Lexicographic path order with status [19].
Precedence:

s₁ > INC₁

Status:

INC₁: [1]
s₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.